YES 1.2510000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| (((==) :: Eq a => a -> a -> Bool) :: Eq a => a -> a -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| (((==) :: Eq a => a -> a -> Bool) :: Eq a => a -> a -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| ((==) :: Eq a => a -> a -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2400), Succ(xv40000)) → new_primPlusNat(xv2400, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2400), Succ(xv40000)) → new_primPlusNat(xv2400, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv3000), Succ(xv4000)) → new_primMulNat(xv3000, Succ(xv4000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv3000), Succ(xv4000)) → new_primMulNat(xv3000, Succ(xv4000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv300), Succ(xv400)) → new_primEqNat(xv300, xv400)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv300), Succ(xv400)) → new_primEqNat(xv300, xv400)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(ty_@2, fh), ga), ea) → new_esEs1(xv31, xv41, fh, ga)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(app(ty_@3, hh), baa), bab), hg) → new_esEs0(xv30, xv40, hh, baa, bab)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(ty_Maybe, bbh)) → new_esEs3(xv31, xv41, bbh)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_Either, he), hf), hg) → new_esEs(xv30, xv40, he, hf)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_Maybe, eh), dh, ea) → new_esEs3(xv30, xv40, eh)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_Maybe, bda)) → new_esEs3(xv30, xv40, bda)
new_esEs3(Just(xv30), Just(xv40), app(app(ty_@2, bdh), bea)) → new_esEs1(xv30, xv40, bdh, bea)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_Either, df), dg), dh, ea) → new_esEs(xv30, xv40, df, dg)
new_esEs(Left(xv30), Left(xv40), app(app(ty_@2, bg), bh), bc) → new_esEs1(xv30, xv40, bg, bh)
new_esEs3(Just(xv30), Just(xv40), app(ty_[], beb)) → new_esEs2(xv30, xv40, beb)
new_esEs(Right(xv30), Right(xv40), cc, app(ty_Maybe, de)) → new_esEs3(xv30, xv40, de)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xv30, xv40, bcc, bcd, bce)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_[], eg), dh, ea) → new_esEs2(xv30, xv40, eg)
new_esEs(Right(xv30), Right(xv40), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv30, xv40, cf, cg, da)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(ty_Either, gd), ge)) → new_esEs(xv32, xv42, gd, ge)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(ty_Maybe, baf), hg) → new_esEs3(xv30, xv40, baf)
new_esEs(Left(xv30), Left(xv40), app(ty_[], ca), bc) → new_esEs2(xv30, xv40, ca)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(ty_[], bae), hg) → new_esEs2(xv30, xv40, bae)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(app(ty_@3, fd), ff), fg), ea) → new_esEs0(xv31, xv41, fd, ff, fg)
new_esEs(Left(xv30), Left(xv40), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xv30, xv40, bd, be, bf)
new_esEs3(Just(xv30), Just(xv40), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs0(xv30, xv40, bde, bdf, bdg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(ty_Maybe, gc), ea) → new_esEs3(xv31, xv41, gc)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(ty_[], bbg)) → new_esEs2(xv31, xv41, bbg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(ty_Maybe, hd)) → new_esEs3(xv32, xv42, hd)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_Either, bca), bcb)) → new_esEs(xv30, xv40, bca, bcb)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(ty_@2, bbe), bbf)) → new_esEs1(xv31, xv41, bbe, bbf)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(ty_@2, ha), hb)) → new_esEs1(xv32, xv42, ha, hb)
new_esEs(Right(xv30), Right(xv40), cc, app(ty_[], dd)) → new_esEs2(xv30, xv40, dd)
new_esEs(Right(xv30), Right(xv40), cc, app(app(ty_Either, cd), ce)) → new_esEs(xv30, xv40, cd, ce)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(ty_[], gb), ea) → new_esEs2(xv31, xv41, gb)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_@2, bcf), bcg)) → new_esEs1(xv30, xv40, bcf, bcg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(app(ty_@3, gf), gg), gh)) → new_esEs0(xv32, xv42, gf, gg, gh)
new_esEs2(:(xv30, xv31), :(xv40, xv41), bdb) → new_esEs2(xv31, xv41, bdb)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, bac), bad), hg) → new_esEs1(xv30, xv40, bac, bad)
new_esEs3(Just(xv30), Just(xv40), app(ty_Maybe, bec)) → new_esEs3(xv30, xv40, bec)
new_esEs(Left(xv30), Left(xv40), app(ty_Maybe, cb), bc) → new_esEs3(xv30, xv40, cb)
new_esEs3(Just(xv30), Just(xv40), app(app(ty_Either, bdc), bdd)) → new_esEs(xv30, xv40, bdc, bdd)
new_esEs(Right(xv30), Right(xv40), cc, app(app(ty_@2, db), dc)) → new_esEs1(xv30, xv40, db, dc)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(ty_[], hc)) → new_esEs2(xv32, xv42, hc)
new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_[], bch)) → new_esEs2(xv30, xv40, bch)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_@2, ee), ef), dh, ea) → new_esEs1(xv30, xv40, ee, ef)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(ty_Either, fb), fc), ea) → new_esEs(xv31, xv41, fb, fc)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(ty_Either, bah), bba)) → new_esEs(xv31, xv41, bah, bba)
new_esEs(Left(xv30), Left(xv40), app(app(ty_Either, ba), bb), bc) → new_esEs(xv30, xv40, ba, bb)
new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(app(ty_@3, eb), ec), ed), dh, ea) → new_esEs0(xv30, xv40, eb, ec, ed)
new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs0(xv31, xv41, bbb, bbc, bbd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs3(Just(xv30), Just(xv40), app(app(ty_@2, bdh), bea)) → new_esEs1(xv30, xv40, bdh, bea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv30), Just(xv40), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs0(xv30, xv40, bde, bdf, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_@2, bcf), bcg)) → new_esEs1(xv30, xv40, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xv30, xv40, bcc, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(xv30), Just(xv40), app(ty_Maybe, bec)) → new_esEs3(xv30, xv40, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_Maybe, bda)) → new_esEs3(xv30, xv40, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(xv30), Just(xv40), app(ty_[], beb)) → new_esEs2(xv30, xv40, beb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(xv30), Just(xv40), app(app(ty_Either, bdc), bdd)) → new_esEs(xv30, xv40, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv30, xv31), :(xv40, xv41), app(app(ty_Either, bca), bcb)) → new_esEs(xv30, xv40, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(ty_@2, fh), ga), ea) → new_esEs1(xv31, xv41, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(ty_@2, ha), hb)) → new_esEs1(xv32, xv42, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_@2, ee), ef), dh, ea) → new_esEs1(xv30, xv40, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(ty_@2, bbe), bbf)) → new_esEs1(xv31, xv41, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, bac), bad), hg) → new_esEs1(xv30, xv40, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Left(xv30), Left(xv40), app(app(ty_@2, bg), bh), bc) → new_esEs1(xv30, xv40, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(xv30), Right(xv40), cc, app(app(ty_@2, db), dc)) → new_esEs1(xv30, xv40, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(app(ty_@3, fd), ff), fg), ea) → new_esEs0(xv31, xv41, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(app(ty_@3, gf), gg), gh)) → new_esEs0(xv32, xv42, gf, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(app(ty_@3, eb), ec), ed), dh, ea) → new_esEs0(xv30, xv40, eb, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_Maybe, eh), dh, ea) → new_esEs3(xv30, xv40, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(ty_Maybe, gc), ea) → new_esEs3(xv31, xv41, gc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(ty_Maybe, hd)) → new_esEs3(xv32, xv42, hd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(ty_[], eg), dh, ea) → new_esEs2(xv30, xv40, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(ty_[], gb), ea) → new_esEs2(xv31, xv41, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(ty_[], hc)) → new_esEs2(xv32, xv42, hc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), app(app(ty_Either, df), dg), dh, ea) → new_esEs(xv30, xv40, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, dh, app(app(ty_Either, gd), ge)) → new_esEs(xv32, xv42, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv40, xv41, xv42), fa, app(app(ty_Either, fb), fc), ea) → new_esEs(xv31, xv41, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(app(ty_@3, hh), baa), bab), hg) → new_esEs0(xv30, xv40, hh, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs0(xv31, xv41, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(ty_Maybe, bbh)) → new_esEs3(xv31, xv41, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(ty_Maybe, baf), hg) → new_esEs3(xv30, xv40, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(ty_[], bae), hg) → new_esEs2(xv30, xv40, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(ty_[], bbg)) → new_esEs2(xv31, xv41, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_Either, he), hf), hg) → new_esEs(xv30, xv40, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv30, xv31), @2(xv40, xv41), bag, app(app(ty_Either, bah), bba)) → new_esEs(xv31, xv41, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Right(xv30), Right(xv40), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv30, xv40, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(Left(xv30), Left(xv40), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xv30, xv40, bd, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Right(xv30), Right(xv40), cc, app(ty_Maybe, de)) → new_esEs3(xv30, xv40, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(xv30), Left(xv40), app(ty_Maybe, cb), bc) → new_esEs3(xv30, xv40, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Left(xv30), Left(xv40), app(ty_[], ca), bc) → new_esEs2(xv30, xv40, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(xv30), Right(xv40), cc, app(ty_[], dd)) → new_esEs2(xv30, xv40, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Right(xv30), Right(xv40), cc, app(app(ty_Either, cd), ce)) → new_esEs(xv30, xv40, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(xv30), Left(xv40), app(app(ty_Either, ba), bb), bc) → new_esEs(xv30, xv40, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv30, xv31), :(xv40, xv41), bdb) → new_esEs2(xv31, xv41, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs2(:(xv30, xv31), :(xv40, xv41), app(ty_[], bch)) → new_esEs2(xv30, xv40, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3